Nuprl Lemma : dset_set_wf
13,42
postcript
pdf
s
:DSet,
Q
:(|
s
|
). {
x
:
s
|
Q
(
x
) }
DSet
latex
Up
sets
1
Definitions of Statement
|
p
|
,
=
,
DSet
,
mk_dset(
T
,
eq
)
,
{
x
:
s
|
Q
(
x
) }
Definitions
suptype(
S
;
T
)
,
S
T
,
x
(
s
)
,
{
x
:
s
|
Q
(
x
) }
,
t
T
,
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
IsEqFun(
T
;
eq
)
,
P
Q
,
DSet
Lemmas
dset
wf
,
bool
wf
,
set
eq
wf
,
set
car
wf
,
mk
dset
wf
,
eqfun
p
subtyping
,
assert
of
dset
eq
origin
s:DSet, Q:(|s|
). {x:s| Q(x) } 
DSet s:DSet, Q:(|s|). {x:s| Q(x) } DSet 
T Tx:A. B(x)
x. t(x)
Q